M:MsgA, k:Knd. k declared in M  M.da(k) = Top  Type 

latex

Definitions	Top, t  T, x:A. B(x), b, A, b, , Prop, False, P  Q, Knd, x. t(x), a:A fp B(a), KindDeq, x  dom(f), P & Q, P  Q, Unit, f(x)?z, M.da(a), k declared in M, MsgA
Lemmas	msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf, top wf